Inference at * 1 
Iof proof for Lemma can-apply-mu':



1. A : Type
2. P : A
3. d : x:A. Dec(n:. ((P(x,n))))
4. x : A
  (isl((TERMOF{p-mu-decider:ObjectId, 1:l, i:l}(A,P,d,x)).1))  (n:. ((P(x,n)))) 

latex

 by (GenConclAtAddr [1;1;1;1]) 
CollapseTHEN ((Thin (-1)) 
CollapseTHEN (((D (-1)) 

CoCollapseTHEN (Reduce 0)) 
CollapseTHEN (((D (-2)) 
CollapseTHEN (Reduce 0)) 
CollapseTHEN (
C(RepUR ``p-mu`` ( -1)) 
CollapseTHEN (MaAuto))))) 

latex

C1: 

C1: 5. Top
C1: 6. i:. ((P(x,i)))
C1: 7. n:. ((P(x,n)))
C1:   False
C.

Definitions	s = t, p-mu-decider, , , left + right, A c B, True, {x:A| B(x)} , p-mu(P;x), P  Q, P & Q, P  Q, P  Q, x:A. B(x), if b then t else f fi , False, Top, x:A.B(x), Dec(P), A, x:AB(x), Type, x:A  B(x), , b, x:A. B(x), f(a), t  T
Lemmas	p-mu-decider, bool wf, decidable wf, top wf, p-mu wf, true wf, false wf, nat wf, assert wf